i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), k:Knd, l:IdLnk, tg:Id, n:,
f:(State(ds)Valtype(da;k)da(rcv(l,tg))?!Void()), es:ES.
(source(l) = i)
 es-decls(es;i;ds;da)
 (@i[[A;k sends on l with tag tg [s,v.f(s,v)], at marker n]]
  es-sends-iff2(es;l;tg;da(rcv(l,tg))?Top;ds;e.kind(e) = k
  & ecl-es-act(es;n;A)(es-init(es;e),e);e.f((state when e),val(e)))) 

latex

Definitions

x:A. B(x), A c B, P  Q, es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e)), Valtype(da;k), Knd, x,y. t(x;y), x(s1,s2), P  Q, P & Q, P  Q, x. t(x), , {T}, SQType(T), t  T, P  Q, x:A. B(x), False, A, Dec(P), x(s)

Lemmas

es-lnk wf, fpf-sub weakening, subtype-fpf-cap-void, decidable equal Id, Knd sq, es-vartype wf, es-state-subtype, es-state-when wf, es-val wf, es-kind wf, es-kind-rcv, es-sender wf, es-loc-init, es-init wf, es-valtype wf, es-isrcv wf, assert wf, ecl-es-act wf, es-loc wf, alle-at wf, es-decls-iff, msg-spec1 wf, ecl-mng-sends wf, fpf wf, ecl wf, IdLnk wf, nat wf, rcv wf, Kind-deq wf, Knd wf, fpf-cap wf, ma-valtype wf, decl-state wf, event system wf, lsrc wf, Id wf, es-decls wf, ecl-mng-sends-single, Id sq, es-sends-iff-bact